k:, f:({0..k}). size(k;f)  {0..(k+1)} 

latex

Definitions	x:A. B(x), t  T, size(k;f), primrec(n;b;c), if b then t else f fi , Y, (i = j), tt, P  Q, i  j , A  B, A, False, {i..j}, i  j < k, P & Q, ,
Lemmas	nat wf, nat properties, ge wf, le wf, int seg wf, bool wf